
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Translation.ErgoNNRCtoJavaScript</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Translation.ErgoNNRCtoJavaScript" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Translation.ErgoNNRCtoJavaScript</h1>
<div class="coq">
<br/>
<div class="doc">Translates ErgoNNRC to JavaScript </div>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html">ErgoSpec.Common.Utils.Misc</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html">ErgoSpec.ErgoNNRC.Lang.ErgoNNRC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoNNRCtoJavaScript">ErgoNNRCtoJavaScript</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string_scope</span>.<br/>
<br/>
<div class="doc">Top-level expression </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_of_expression">javascript_of_expression</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_expr">nnrc_expr</a></span>)                  <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                      <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">i</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                      <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)                   <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)                <br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.nnrc_expr_javascript_unshadow">ErgoCodeGen.nnrc_expr_javascript_unshadow</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#e">e</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
<div class="doc">Top-level constant </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_of_constant">javascript_of_constant</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">v</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)                     <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">bind</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_expr">nnrc_expr</a></span>)               <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                      <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">i</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                      <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)                   <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)                <br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">s1</span>, <span class="id">e1</span>, <span class="id">t2</span>) := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.nnrc_expr_to_javascript">ErgoCodeGen.nnrc_expr_to_javascript</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#bind">bind</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">v0</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> ("<span class="id">v</span>" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#v">v</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">s1</span> ++ (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_indent">ErgoCodeGen.javascript_indent</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span>) ++ "<span class="id">var</span> " ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#v0">v0</a></span> ++ " = " ++ <span class="id">e1</span> ++ ";" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#v0">v0</a></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">t2</span>).<br/>
<br/>
<div class="doc">Single method </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_method_of_body">javascript_method_of_body</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_expr">nnrc_expr</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">input_v</span> := "<span class="id">context</span>" <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.nnrc_expr_to_javascript_method">ErgoCodeGen.nnrc_expr_to_javascript_method</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#input_v">input_v</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#e">e</a></span> 1 <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#input_v">input_v</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#fname">fname</a></span>).<br/>
<br/>
<div class="doc">Single function </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_function_of_body">javascript_function_of_body</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_expr">nnrc_expr</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">input_v</span> := "<span class="id">context</span>" <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_indent</span> := 0 <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.nnrc_expr_to_javascript_fun_lift">ErgoCodeGen.nnrc_expr_to_javascript_fun_lift</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#e">e</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#fname">fname</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#input_v">input_v</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#init_indent">init_indent</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_function_of_nnrc_function">javascript_function_of_nnrc_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_function">nnrc_function</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fname</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#function_name_in_table">function_name_in_table</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#tname">tname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#functionn_name">functionn_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_function_of_body">javascript_function_of_body</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#functionn_lambda">functionn_lambda</a></span>).(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#lambdan_body">lambdan_body</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#fname">fname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_method_of_nnrc_function">javascript_method_of_nnrc_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_function">nnrc_function</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fname</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#functionn_name">functionn_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_method_of_body">javascript_method_of_body</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#functionn_lambda">functionn_lambda</a></span>).(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#lambdan_body">lambdan_body</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#fname">fname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_methods_of_nnrc_functions">javascript_methods_of_nnrc_functions</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fl</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_function">nnrc_function</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Misc.html#multi_append">multi_append</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> (<span class="kwd">fun</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_method_of_nnrc_function">javascript_method_of_nnrc_function</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#fl">fl</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_class_of_nnrc_function_table">javascript_class_of_nnrc_function_table</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ft</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_function_table">nnrc_function_table</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">tname</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_identifier_sanitizer">ErgoCodeGen.javascript_identifier_sanitizer</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#ft">ft</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#function_tablen_name">function_tablen_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">class</span> " ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#tname">tname</a></span> ++ " {" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_methods_of_nnrc_functions">javascript_methods_of_nnrc_functions</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#ft">ft</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#function_tablen_funs">function_tablen_funs</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#tname">tname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>) ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "}" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="preamble">preamble</a></span> (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;"" ++ "'<span class="id">use</span> <span class="id">strict</span>';" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "/*<span class="id">eslint</span>-<span class="id">disable</span> <span class="id">no</span>-<span class="id">unused</span>-<span class="id">vars</span>*/" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "/*<span class="id">eslint</span>-<span class="id">disable</span> <span class="id">no</span>-<span class="id">undef</span>*/" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "/*<span class="id">eslint</span>-<span class="id">disable</span> <span class="id">no</span>-<span class="id">var</span>*/" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="postamble">postamble</a></span> (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;"" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "/*<span class="id">eslint</span>-<span class="id">enable</span> <span class="id">no</span>-<span class="id">unused</span>-<span class="id">vars</span>*/" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "/*<span class="id">eslint</span>-<span class="id">enable</span> <span class="id">no</span>-<span class="id">undef</span>*/" ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_of_declaration">javascript_of_declaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">s</span> : <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_declaration">nnrc_declaration</a></span>)   <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">i</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span>          <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span>        <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>                           <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#s">s</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#DNExpr">DNExpr</a></span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_of_expression">javascript_of_expression</a></span> <span class="id">e</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#DNConstant">DNConstant</a></span> <span class="id">v</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_of_constant">javascript_of_constant</a></span> <span class="id">v</span> <span class="id">e</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#DNFunc">DNFunc</a></span> <span class="id">f</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_function_of_nnrc_function">javascript_function_of_nnrc_function</a></span> <span class="id">f</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>,"<span class="id">null</span>",<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#DNFuncTable">DNFuncTable</a></span> <span class="id">ft</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_class_of_nnrc_function_table">javascript_class_of_nnrc_function_table</a></span> <span class="id">ft</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>,"<span class="id">null</span>",<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="javascript_of_declarations">javascript_of_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sl</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_declaration">nnrc_declaration</a></span>) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">t</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                    <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">i</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>)                    <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="kwd">let</span> <span class="id">proc_one</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">s</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_declaration">nnrc_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">s0</span>, <span class="id">t0</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#acc">acc</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">s1</span>, <span class="id">e1</span>, <span class="id">t1</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_of_declaration">javascript_of_declaration</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#s">s</a></span> <span class="id">t0</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#i">i</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">s0</span> ++ <span class="id">s1</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">t1</span>) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">sn</span>, <span class="id">tn</span>) := <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#proc_one">proc_one</a></span> ("",<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#t">t</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#sl">sl</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">sn</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="nnrc_module_to_javascript">nnrc_module_to_javascript</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_module">nnrc_module</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#preamble">preamble</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>) ++ <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#javascript_of_declarations">javascript_of_declarations</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#modulen_declarations">modulen_declarations</a></span>) 0 0 <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#quotel">quotel</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#postamble">postamble</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#eol">eol</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="nnrc_module_to_javascript_top">nnrc_module_to_javascript_top</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.html#nnrc_module">nnrc_module</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript">ErgoCodeGen.javascript</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#nnrc_module_to_javascript">nnrc_module_to_javascript</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#p">p</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_eol_newline">ErgoCodeGen.javascript_eol_newline</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCodeGen.javascript_quotel_double">ErgoCodeGen.javascript_quotel_double</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNNRCtoJavaScript.html#ErgoNNRCtoJavaScript">ErgoNNRCtoJavaScript</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
